[Civl] Fix to heuristic for variable elimination in transition relation computation #677
Conversation
| if (trc.allLocVars.Count > 0) | ||
| { | ||
| for (int i = 1; i <= trc.allLocVars.Select(v => varCopies[v].Count).Max(); i++) | ||
| { | ||
| TryElimination(trc.allLocVars.SelectMany(v => | ||
| varCopies[v].GetRange(0, i <= varCopies[v].Count ? i : varCopies[v].Count))); | ||
| } | ||
| } |
There was a problem hiding this comment.
Took me a minute to understand. Maybe a comment explaining that we are eliminating with increasing sets of copies (copies 0, copies 0+1, ...) would be helpful. Two minor suggestions:
- Extract
trc.allLocVars.Select(v => varCopies[v].Count).Max()to a variable. - Replace
i <= varCopies[v].Count ? i : varCopies[v].CountwithMath.min(i, varCopies[v].Count).
Is there an intuitive reason why exactly this heuristic? I get that the initial copies and final copies belong together, since they form the pre and post state. But is there something that connects the i-th copies?
There was a problem hiding this comment.
@bkragl : Thanks so much for attempting to understand this modification. After my first attempt, I realized that my intention was to do something else. I have pushed a revision, this time including some comments. Let me know what you think.
| assert Init(pids, ReqCH, QuoteCH, RemCH, DecCH, contribution); | ||
| QuoteCH := (lambda i:int :: (lambda q:int :: if buyerID(i) && q == price then 1 else 0)); | ||
| assume {:add_to_pool "contribution", contribution} true; |
There was a problem hiding this comment.
Would it make sense to attach the add_to_pool attribute to the assertion or better keep it separate? Wondering if there is any convention.
There was a problem hiding this comment.
I have recently realized that putting :add_to_pool annotations on asserts in the body of atomic actions is not being handled correctly since I added the HoistAsserts code. This code is not propagating the attributes on the asserts as it hoists them.
I am unsure what to do. I am thinking about restricting the scope of add_to_pool even further in the documentation allowing them to be used only on assume commands.
| @@ -1,2 +1,2 @@ | |||
|
|
|||
| Boogie program verifier finished with 130 verified, 0 errors | |||
| Boogie program verifier finished with 132 verified, 0 errors | |||
There was a problem hiding this comment.
I don't know. I was mystified too.
| @@ -47,13 +47,12 @@ function max(CH:[val]int) : val; | |||
| function card(CH:[val]int) : int; | |||
|
|
|||
| axiom card(MultisetEmpty) == 0; | |||
| axiom (forall v:val :: card(MultisetSingleton(v)) == 1); | |||
| axiom (forall CH:[val]int, v:val :: card(MultisetPlus(CH, MultisetSingleton(v))) == card(CH) + 1); | |||
There was a problem hiding this comment.
On my machine this axiom can be removed too.
| axiom (forall CH:[val]int, v:val :: card(MultisetPlus(CH, MultisetSingleton(v))) == card(CH) + 1); | ||
| axiom (forall CH:[val]int, v:val :: {CH[v := CH[v] + 1]} card(CH[v := CH[v] + 1]) == card(CH) + 1); | ||
| axiom (forall m:[val]int, m':[val]int :: {card(m), card(m')} MultisetSubsetEq(m, m') && card(m) == card(m') ==> m == m'); | ||
| axiom (forall CH:[val]int, v:val, x:int :: card(CH[v := x]) == card(CH) + x - CH[v]); |
|
|
||
| axiom (forall v:val :: max(MultisetSingleton(v)) == v); | ||
| axiom (forall CH:[val]int, v:val :: { CH[v := CH[v] + 1] } max(CH[v := CH[v] + 1]) == (if v > max(CH) then v else max(CH))); | ||
| axiom (forall CH:[val]int, v:val, x:int :: max(CH[v := x]) == (if v > max(CH) && x > 0 then v else max(CH))); |
There was a problem hiding this comment.
nit: make x > 0 the lhs of an implication
shazqadeer
force-pushed
the
sample-refactor
branch
from
0e0366b to
805300a
Compare
fix to heuristic for variable elimination
shazqadeer
force-pushed
the
sample-refactor
branch
from
805300a to
19bd5d1
Compare
The investigation behind this PR started when I attempted to eliminate the duplication between the abstract and concrete actions used in the IS proof of NBuyer. I wanted to simply call the concrete atomic action from the abstract one right after the extra asserts had been added. I discovered that the refactored code did not verify due to proof flakiness. The changes to the sample were my efforts (not all of which may have been necessary) to reduce the flakiness while still achieving no duplication of code. In the process, I also attempted to generalize the heuristic for variable elimination in computation of transition relations. The revised (more powerful) heuristic is needed for the revised version of NBuyer.bpl otherwise the cooperation check for MiddleBuyer' does not verify.
The change to transition relation computation is in the second attempt to eliminate temporaries. Before this PR, the second attempt used as defined only the initial incarnations of locals. The PR changes this logic to allow as defined any incarnation that does not have a definition among assignments. Thus, all incarnations generated by havocs are also considered as defined.
While working on this PR, I discovered that the computation of transition relation of atomic actions also uses patterns. The triggers for these patterns are injected in the body of atomic actions. The instantiation induced by these triggers is more precise than what is achievable today via pools. Furthermore, the triggers appear to be needed for the verification of commutativity checks. This PR also modifies the trigger generation. Before this PR, triggers were being generated only for the initial incarnation of local variables. This PR adds trigger generation for incarnations created due to havoc commands as well. Live variable analysis is done over the body of atomic actions to avoid adding triggers for incarnations that are not live. This optimization appears to be important for the commutativity check between A_Propose and A_Propose'. This check quickly starts to become expensive with more instantiations, either due to triggers or due to pools. This explosive growth in running time is a ticking time bomb in the scalability of Civl.
The overall effect of this PR is to eliminate the duplication between concrete and abstract actions across our entire set of benchmarks.